Nuprl Lemma : es-shift_wf
11,40
postcript
pdf
T
:(Id
Type),
s
:EState(
T
),
r
:rationals.
s
+
r
EState(
T
)
latex
Definitions
EState(
T
)
,
s
+
r
,
x
.
A
(
x
)
,
r
+
s
,
x
:
A
.
B
(
x
)
,
rationals
,
f
(
a
)
,
x
:
A
B
(
x
)
,
Id
,
t
T
,
Type
Lemmas
Id
wf
,
rationals
wf
,
qadd
wf
origin
T:(Id
Type), s:EState(T), r:rationals. s+r 
EState(T) T:(IdType), s:EState(T), r:rationals. s+r EState(T) 
x.A(x)x:A. B(x)B(x) T